<html>
<head><meta charset="utf-8"><title>the meaning of not · wg-traits · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/index.html">wg-traits</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html">the meaning of not</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="184164396"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184164396" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184164396">(Dec 24 2019 at 11:32)</a>:</h4>
<p><span class="user-mention" data-user-id="232957">@Jack Huey</span> Let's discuss the meaning of <code>not</code> a bit. I've been pondering it indeed.</p>



<a name="184164412"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184164412" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184164412">(Dec 24 2019 at 11:33)</a>:</h4>
<p><a href="http://aturon.github.io/tech/2017/04/24/negative-chalk/" target="_blank" title="http://aturon.github.io/tech/2017/04/24/negative-chalk/">Aaron's blog post</a> describes "modal logic":</p>
<blockquote>
<p>Modal logic makes truth relative to a possible world, rather than being an absolute thing. In one world, the sky is blue; in another world, it’s red. That’s the story for “facts”. But the basic rules of logic apply no matter what world you’re talking about: 1+1 = 2 in every possible world.</p>
</blockquote>



<a name="184164420"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184164420" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184164420">(Dec 24 2019 at 11:33)</a>:</h4>
<p>In Rust terms, we have to ask ourselves in what "world" we are trying to prove things</p>



<a name="184164472"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184164472" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184164472">(Dec 24 2019 at 11:34)</a>:</h4>
<p>In <span class="user-mention" data-user-id="117350">@Sunjay Varma</span>'s work on coherence, we introduced this idea of a "compatible" mode. It means basically "we're trying to prove whether this impl exists in any semver-compatible world". That turns out to be a much broader set of impls, of course, than the ones we can see. It includes downstream crates, for example.</p>



<a name="184164480"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184164480" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184164480">(Dec 24 2019 at 11:35)</a>:</h4>
<p>We <em>implement</em> this in chalk via a special predicate (<code>Compatible</code>) that can ordinarily not be proven, but which can be inserted into the environment. So <code>Compatible =&gt; G</code> means "is G true for all semver-compatible worlds?"</p>



<a name="184164490"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184164490" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184164490">(Dec 24 2019 at 11:35)</a>:</h4>
<p>Just proving <code>G</code> means "is G true in this world -- i.e., for the impls and assumptions we can see right now?"</p>



<a name="184164564"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184164564" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184164564">(Dec 24 2019 at 11:36)</a>:</h4>
<p>Another good read is the "Negation as Failure" paper, though I can't find a free PDF of it (I think I bought it at some point)</p>



<a name="184164591"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184164591" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184164591">(Dec 24 2019 at 11:37)</a>:</h4>
<p>Negation as failure means the idea of saying "if I can't find prove G, it must be false". This is the traditional Prolog form. It makes some sense because Prolog is <em>complete</em> -- i.e., if it can't prove something, there is no solution.</p>



<a name="184164674"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184164674" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184164674">(Dec 24 2019 at 11:39)</a>:</h4>
<p>But chalk is a superset of prolog and indeed the interaction of negation-as-failure with <code>forall</code> feels kind of complex. For example, should <code>forall&lt;T&gt; { not { T: Iterator } }</code> be true? Seems like probably <em>not</em> -- we don't know that <code>T: Iterator</code>, but we also don't know that it <em>doesn't</em>.</p>
<p>But what about if there are no <code>Iterator</code> impls in the program at all?</p>



<a name="184164859"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184164859" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184164859">(Dec 24 2019 at 11:43)</a>:</h4>
<p>I came up against this yeah because I've been pondering this test-case:</p>
<div class="codehilite"><pre><span></span>forall&lt;T&gt; {
    not { &lt;T as Foo&lt;i32&gt;&gt;::Bar = &lt;T as Foo&lt;u32&gt;&gt;::Bar }
}
</pre></div>


<p>right now this is provable, at least <em>sometimes</em>, which sort of seems wrong. But then, what if there are no impls of <code>Foo</code> at all? Or no impls where <code>Bar</code> is defined to be the same type?</p>



<a name="184164903"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184164903" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184164903">(Dec 24 2019 at 11:44)</a>:</h4>
<p>And indeed I think if there <em>is</em> an impl where <code>Bar</code> overlaps, then we get it right.</p>



<a name="184164928"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184164928" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184164928">(Dec 24 2019 at 11:45)</a>:</h4>
<p>So it seems like the question is, to some extent, in what "world" are we checking negation (or perhaps, checking generic functions). This then circles back a bit to "for what purpose are we <em>using</em> negation"?</p>



<a name="184165003"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184165003" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184165003">(Dec 24 2019 at 11:47)</a>:</h4>
<p>(One problem we had early on was that <code>forall&lt;T, U&gt; { not { T = U } }</code> would be provable, which seems clearly wrong; we resolved this by the current method of replacing placeholders with inference variablles when negating, though we considered other approaches. I just had a branch where I was exploring the problem above and I was considering whether to revive some of the older approaches when I realized that it wasn't entirely clear to me what behavior I felt was "right")</p>



<a name="184165208"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184165208" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184165208">(Dec 24 2019 at 11:53)</a>:</h4>
<p>I think the main uses we have for negation are:</p>
<ul>
<li>coherence</li>
<li>specialization -- still needs to be elaborated!</li>
<li>maybe playing some role in projection</li>
</ul>



<a name="184179291"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184179291" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184179291">(Dec 24 2019 at 17:01)</a>:</h4>
<p><code>not</code> has always thrown me for a loop</p>



<a name="184179336"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184179336" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184179336">(Dec 24 2019 at 17:02)</a>:</h4>
<p>especially when in the context of <code>exists</code> or <code>forall</code></p>



<a name="184179393"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184179393" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184179393">(Dec 24 2019 at 17:03)</a>:</h4>
<p>This sort of train of thought reminds me of when you said something to the extent of "I would rather make all traits non-enumerable"</p>



<a name="184179446"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184179446" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184179446">(Dec 24 2019 at 17:04)</a>:</h4>
<p>In that, when we solve these goals, what are we considering? The current <em>known</em> world? Or the set of <em>possible</em> worlds?</p>



<a name="184179492"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184179492" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184179492">(Dec 24 2019 at 17:05)</a>:</h4>
<p>And, sure, Rust has a set of coherence rules that <em>limit</em> that set of possible worlds, but in the end, I think it would/should ultimately be the difference between a "suggestion" and a "unique answer"</p>



<a name="184179493"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184179493" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184179493">(Dec 24 2019 at 17:05)</a>:</h4>
<p>maybe?</p>



<a name="184179538"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184179538" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184179538">(Dec 24 2019 at 17:06)</a>:</h4>
<p>Anyways, bringing it back to <code>not</code></p>



<a name="184179644"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184179644" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184179644">(Dec 24 2019 at 17:08)</a>:</h4>
<p>I might take a look at coherence rules a bit closer (more specifically, how they're written in Chalk) and <code>Compatible</code></p>



<a name="184186403"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184186403" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184186403">(Dec 24 2019 at 19:54)</a>:</h4>
<blockquote>
<p>But chalk is a superset of prolog and indeed the interaction of negation-as-failure with <code>forall</code> feels kind of complex. For example, should <code>forall&lt;T&gt; { not { T: Iterator } }</code> be true? Seems like probably <em>not</em> -- we don't know that <code>T: Iterator</code>, but we also don't know that it <em>doesn't</em>.</p>
<p>But what about if there are no <code>Iterator</code> impls in the program at all?</p>
</blockquote>
<p>So, I've been thinking  about this. Why <em>aren't</em> are Chalk goals and program "complete"? I would say that is the point of the <code>Compatible</code> predicate  right? That we either <em>enumerate</em> all possible impls or we say "something impls <code>Iterator</code>, but we can't prove it"?</p>



<a name="184196700"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/the%20meaning%20of%20not/near/184196700" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Charles Lew <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/the.20meaning.20of.20not.html#184196700">(Dec 25 2019 at 01:29)</a>:</h4>
<p>I want to share my very naive view on this. (Ignore me if my theory goes too wrong). So we can see a Rust program as a series of "claim"s, the programmer thought they're facts, but maybe they're not, and it's the compiler's duty to find out. Two "claim"s may conflict with each other, and human may come up with a negative example for one "claim".</p>
<p>So in my mindset every query to chalk should be the form:</p>
<p>not (Contradiction) &amp;&amp; { ConcreteType($TypeLevelExpr, ?Result) }</p>
<p>where Contradiction is a special predicate that when proved, it means that the "repo" itself is not in a consistent state, e.g. there're two claims in it that each conflicts with the other.</p>
<p>and about the "not" construct, i think it's composed with two smaller goals:<br>
not A :- CannotProveUnderAssumption(True, A) &amp;&amp; CannotProveUnderAssumption(!A, Contradiction)</p>
<p>where CannotProveUnderAssumption is a special predicate that represents the capability of Chalk itself.</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>